(declare-const x30 Bool)
(declare-const x Float64)
(declare-const x3 Bool)
(declare-const x32 Bool)
(declare-fun r2 () Float64)
(declare-fun a () (_ BitVec 64))
(declare-fun r1 () Float64)
(declare-fun r () RoundingMode)
(assert (xor x32 x30 (fp.gt (_ +zero 11 53) x)))
(assert x3)
(assert (and (= r2 ((_ to_fp 11 53) r 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000.0)) (bvslt (bvadd (_ bv4294966273 32) ((_ extract 63 32) a)) (_ bv0 32)) (fp.gt (fp.add r r1 (fp (_ bv1 1) (_ bv0 11) (_ bv0 52))) (_ +zero 11 53))))
(check-sat)
